#pragma once

#include <vector>
#include <list>
#include "constants.h"
#include "clause.h"
#include "decision.h"
#include "istrategy.h"
#include "problem_variable.h"
#include "conflict.h"
#include <fstream>

namespace solver
{
	class problem_solver;

	class production
	{
	public:
		decision_string match;
		literal product;
		int stringid;
	};

	typedef production *pproduction;


	class problem_solver
	{
	public:
		int index;
		std::string problem_name;
		std::vector<problem_variable> variables;
		std::vector<pdecision> decisions;
		std::vector<pproduction> productions;
		decision_string_collection production_index;
		std::string comments;
		decision_string conflict_literals;
		decision_string solution;

		// our progress in solving!
		pdecision step_clause;
		literal step_literal;


		bool solved;
		bool trace_enabled;
		int trace_index;
		bool trace_started;
		int pass_count;

		problem_solver()
		{
			clear();
		}

		~problem_solver()
		{
			clear();
		}

		void clear()
		{
			pass_count = 0;
			srand(0);
			index = 0;
			solution.clear();
			problem_name.clear();
			variables.clear();
			comments.clear();
			for (int i = 0; i < decisions.size(); i++)
			{
				delete decisions[i];
				decisions[i] = nullptr;
			}
			decisions.clear();
			solved = false;
			trace_enabled = false;
			trace_index = 0;
			trace_started = false;
		}

		bool solve(solver::istrategy& solver_strategy)
		{
			while (step(solver_strategy));

			if (!solved)
			{
				solution.clear();
			}

			return solved;
		}

		bool step(solver::istrategy& solver_strategy)
		{
			pass_count++;
			bool finished = false;
			int s = decisions.size();

			if (guess_solution())
			{
				solved = true;
				finished = true;
			}
			else
			{

			}

			apply_solution(solver_strategy);
			return finished;
		}

	private:

		void apply_solution(solver::istrategy& solver_strategy)
		{
			int s = solution.size();
			int vc = variables.size();
			int ds = decisions.size();
			int i;
			int t;

			for (i = 0; i < ds; i++)
			{
				auto &dec = decisions[i];
				dec->selected_literal = -1;
			}

			for (i = 0; i < vc; i++)
			{
				auto& v = variables[i];
				v.check_valid = true;
				v.value = -1;
			}

			for (auto& ch : solution)
			{
				auto& v = variables[ch.ref];
				t = ch.val;

				if (v.check_valid && (v.value == -1 || v.value == t))
				{
					v.value = t;
				}
				else
				{
					v.check_valid = false;
				}

				int ds = decisions.size();
				for (int j = 0; j < ds; j++) 
				{
					auto dec = decisions[j];
					if (dec->selected_literal == -1) 
					{
						for (int i = 0; i < dec->literals.size(); i++)
						{
							if (ch == dec->literals[i]) 
							{
								dec->selected_literal = i;
								break;
							}
						}
					}
				}
			}
		}

		bool guess_solution()
		{
			literal guess;
			bool failed;

			guess = get_next_literal();
			if (guess.ref == -1)
			{
				return true;
			} 
			failed  = apply_literal(guess);

			return false;
		}

		// literal get_next_literal() returns the next literal from the next unsolved clause as a guess.
		// if the returned result is -1, then the problem is solved.
		// todo, accelerate
		literal get_next_literal()
		{
			literal guess;

			int nd = decisions.size();
			for (int i = 0; i < nd; i++)
			{
				decision *dec = decisions[i];
				int nds = dec->literals.size();
				bool found = false;
				for (int j = 0; j < nds && !found; j++)
				{
					if (solution.contains(dec->literals[j])) {
						found = true;
					}
				}
				if (!found)
				{
					for (int j = 0; j < nds && !found; j++)
					{
						guess = dec->literals[j];
						if (!solution.contains(guess)) {
							step_clause = dec;
							step_literal = guess;
							return guess;
						}
					}
				}
			}

			guess.ref = -1;
		}

		bool produces_conflict(decision_string ds)
		{
			int i;

			bool found_matches = false;
			int psz = productions.size();

			do
			{
				std::list<literal_node *> found_strings;
				production_index.find_strings(ds, found_strings);

				found_matches = false;

				for (auto& nd : found_strings)
				{
					found_matches = true;
					auto& prd = productions[nd->string_id];
					if (prd->product.ref > -1)
					{
						ds.add(prd->product);
					}
					else
					{
						return true;
					}
				}
			} while (found_matches);

			return false;
		}

		bool apply_literal(literal guess)
		{
			int i, psz, csz;

			// clear conflicts
			conflict_literals.clear();
			conflict_literals.add(guess);
			solution.add(guess);

			bool found_conflicts = false;
			bool found_matches = false;
			int step_count = 0;

			do 
			{
				std::list<literal_node *> found_strings;
				production_index.find_strings(solution, found_strings);

				found_matches = false;

				for (auto& nd : found_strings)
				{
					auto& prd = productions[nd->string_id];
					found_matches = true;
					if (prd->product.ref > -1)
					{
						solution.add(prd->product);
						if (!step_count)
						{
							conflict_literals.add(prd->product);
						}
					}
					else
					{
						found_conflicts = true;
					}
					if (!step_count)
					{
						auto ndi = nd;
						while (ndi != nullptr)
						{
							conflict_literals.add(ndi->lit);
							ndi = ndi->parent;
						}
					}
				}
				step_count++;
			} while (found_matches);

			// we are conflicted.  we now try to find a resolution to the conflict.
			// if we cannot, we are done.
			std::vector<literal *> resolution;
			int found_lp = decision_string::find_literal_pointers(solution, conflict_literals, resolution);

			bool conflicted = true;
			bool more = true;
			decision_string::clear_literal_pointers(resolution);

			while (conflicted && more)
			{
				if (!produces_conflict(solution))
				{
					conflicted = false;
				}

				more = decision_string::increment_literal_pointers(resolution, 1);
			}

			return conflicted;
		}

	};
}
